Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    is_empty(nil)  → true
2:    is_empty(cons(x,l))  → false
3:    hd(cons(x,l))  → x
4:    tl(cons(x,l))  → l
5:    append(l1,l2)  → ifappend(l1,l2,l1)
6:    ifappend(l1,l2,nil)  → l2
7:    ifappend(l1,l2,cons(x,l))  → cons(x,append(l,l2))
There are 2 dependency pairs:
8:    APPEND(l1,l2)  → IFAPPEND(l1,l2,l1)
9:    IFAPPEND(l1,l2,cons(x,l))  → APPEND(l,l2)
The approximated dependency graph contains one SCC: {8,9}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006